$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$).
\\[0ex]Inj($T$;$T$;$f$) $\Rightarrow$ ($\forall$$x$, $y$:$T$. $x$ is $f$$\ast$($y$) $\Rightarrow$ ($\forall$$z$:$T$. $x$ is $f$$\ast$($z$) $\Rightarrow$ ($z$ is $f$$\ast$($y$) $\vee$ $y$ is $f$$\ast$($z$))))